Nuprl Lemma : kind-rename-inj
11,40
postcript
pdf
ra
,
rt
:(Id
Id). Inj(Id;Id;
rt
)
Inj(Id;Id;
ra
)
Inj(Knd;Knd;
k
.kind-rename(
ra
;
rt
;
k
))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Id
,
s
=
t
,
True
,
T
,
locl(
a
)
,
IdLnk
,
rcv(
l
,
tg
)
,
Knd
,
P
&
Q
,
f
(
a
)
,
{
T
}
,
False
,
x
:
A
B
(
x
)
,
left
+
right
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
x
:
A
B
(
x
)
,
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
Inj(
A
;
B
;
f
)
,
kind-rename(
ra
;
rt
;
k
)
Lemmas
kindcase
wf
,
Knd
wf
,
not
locl
rcv
,
not
rcv
locl
,
locl
one
one
,
rcv
one
one
,
rcv
wf
,
IdLnk
wf
,
locl
wf
,
squash
wf
,
true
wf
,
Id
wf
origin
ra, rt:(Id
Id). Inj(Id;Id;rt) 
Inj(Id;Id;ra) Inj(Knd;Knd;
k.kind-rename(ra;rt;k)) ra, rt:(IdId). Inj(Id;Id;rt) Inj(Id;Id;ra) Inj(Knd;Knd;k.kind-rename(ra;rt;k)) 
T Qx:A. B(x)
T
B(x)B(x)
x,y. t(x;y)x. t(x)